Nuprl Lemma : es-state-ap_wf 11,40

es:ES, i:Id, s:state@ix:Id. s.x  vartype(i;x
latex


DefinitionsES, t  T, Id, Top, x:AB(x), es-T(es), f(a), Type, discrete(i;x), if b then t else f fi , x:AB(x), vartype(i;x), s.x, state@i
Lemmasifthenelse wf, es-isconst wf, es-T wf, top wf, Id wf, event system wf

origin